$\forall$$A$, $B$:Type, ${\it opa}$:($A$$\rightarrow$$A$), ${\it opb}$:($B$$\rightarrow$$B$), $f$:($A$$\rightarrow$$B$). SqStable(fun\_thru\_1op($A$;$B$;${\it opa}$;${\it opb}$;$f$))